package contracts;

import decorators.BombeDecorator;
import services.BombeService;

public class BombeContract extends BombeDecorator implements BombeService{

	public BombeContract(BombeService delegate) {
		super(delegate);
	}

	public void checkInvariant() throws ContractException{
		/*[invariants]
				0 <= getCompteARebours(B) <= 10 */
		if(super.getCompteARebours() < 0){
			throw new InvariantException("Invariant du service Bombe : getCompteARebours ne doit pas etre inferieur a 0");
		} else if(super.getCompteARebours() > 10){
			throw new InvariantException("Invariant du service Bombe : getCompteARebours ne doit pas etre superieur a 10");
		}
		/*		vaExploser(B) = (getCompteARebourds(B) = 0)     =>    minimisation */
		if(!(super.vaExploser() == (super.getCompteARebours() == 0))){
			throw new InvariantException("Invariant du service Bombe : vaExploser n'est pas verifie");
		}
	}
	
	@Override
	public int getNumero(){
		return super.getNumero();
	}
	
	@Override
	public int getX(){
		return super.getX();
	}
	
	@Override
	public int getY(){
		return super.getY();
	}
	
	@Override
	public int getAmplitude(){
		return super.getAmplitude();
	}
	
	@Override
	public int getCompteARebours(){
		return super.getCompteARebours();
	}
	
	@Override
	public void setCompteARebours(int n){
		super.setCompteARebours(n);
	}
	
	@Override
	public boolean vaExploser(){
		return super.vaExploser();
	}
	
	@Override
	public void init(int numero, int x, int y, int amplitude) throws ContractException{
		//\pre init(num, x, y, amplitude) require 3 <= amplitude <= 11
		if(!(amplitude >= 3 && amplitude <= 11)){
			throw new PreconditionException("service Bombe, precondition de init non respectee");
		}
		
		super.init(numero, x, y, amplitude);
		
		this.checkInvariant();
		
		//\post getNumero(init(num, x, y, amplitude)) = num
		if(this.getNumero() != numero){
			throw new PostconditionException("service Bombe, poscondition \"getNumero\" de init non respectee");
		}
		
		//\post getX(init(num, x, y, amplitude)) = x
		if(this.getX() != x){
			throw new PostconditionException("service Bombe, postcondition \"getX\" de init non respectee");
		}
		
		//\post getY(init(num, x, y, amplitude)) = y
		if(this.getY() != y){
			throw new PostconditionException("service Bombe, postcondition \"getY\" de init non respectee");
		}
		
		//\post getAmplitude(init(num, x, y, amplitude)) = amplitude
		if(this.getAmplitude() != amplitude){
			throw new PostconditionException("service Bombe, postcondition \"getAmplitude\" de init non respectee");
		}
		
		//\post getCompteARebours(init(num, x, y, amplitude)) = 10
		if(this.getCompteARebours() != 10){
			throw new PostconditionException("service Bombe, postcondition \"getCompteARebours\" de init non respectee");
		}
	}
}
